COMMENT ⊗   VALID 00020 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00003 00002	.require "memo.pub[let,jmc]" source
C00004 00003	%3Abstract:%1 An Elephant program is a collection of sentences of first
C00007 00004	#. %3Introduction%1
C00012 00005	#. %3Expressing a sequential program in Elephant%1
C00021 00006	#. %3Reversing a list%1
C00026 00007	#. %3Another Elephant Formalism%1
C00032 00008	.if true then begin "defining functions"
C00035 00009	#. %3Equivalence of Elephant programs%1
C00041 00010	#. %3Non Immediate Elephant Programs%1
C00043 00011	#. %3An airline reservation system%1
C00047 00012	.if false then begin
C00051 00013	#. %2samefringe%1
C00055 00014	.<<dining philosophers>>
C00060 00015	#. %3Parallel processes for computing a sum of functions%1
C00065 00016	#. %3Temporal Logic Considered Unnecessary%1
C00077 00017	#. %3Remarks%1
C00084 00018	#. %3References%1
C00088 00019	.if false then begin
C00092 00020	.end
C00096 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source
.every heading (,incomplete draft,{page});
.at "qg" ⊂"%3go_to%*"⊃
.at "qNIL" ⊂"%1NIL%*"⊃
.at "qt" ⊂"%At%*"⊃
.at "qF" ⊂"%AF%*"⊃
.turn on "→"
.group skip 15
.cb THE ELEPHANT LANGUAGE FOR PROVING AND MAYBE EVEN PROGRAMMING
.skip 1
.once center
by John McCarthy


.item←0
%3Abstract:%1 An Elephant program is a collection of sentences of first
order logic.  Corresponding to a program variable ⊗x in an Algol-type
program, there is a function ⊗x(t) of time in the Elephant program.
Sentences of first order logic tell how the values of variables like ⊗x(t) 
depend on the values of the variables at earlier times.  The %2program
counter%1 is treated as just another variable.

	Representing program variables as explicit functions of time has
been explicitly rejected by many computer scientists, but it
has advantages that justify overcoming their prejudices.
  First,
properties of Elephant programs are expressed as first order sentences in
the language of the data domain augmented by the names of the functions
constituting the program.
  The usual methods for proving properties of
programs require no new "logic of programming"; they are just styles of
proof in first order logic.  We make comparisons with temporal logic.
  Second,
equivalences between programs are conveniently expressed and proved.
Third,
 the
sentence representing a combination of flowcharts is just the conjunction
of the sentences representing the flowcharts separately.

	Besides representing ordinary sequential and parallel programs,
Elephant can represent programs that refer to the past of variables and
therefore avoid explicit mention of many data structures.  Since we often
refer to the past in expressing processes in natural language, a computer
language that doesn't allow it cannot claim to be "natural".
.skip to column 1
#. %3Introduction%1
.double space

	The Elephant algorithmic language
represents program variables as functions of a time variable %2t%1.
Instead of a variable ⊗x as in an Algol program, an Elephant program
has a function
⊗x(t), and instead of an assignment statement %2x_:=_...%1, we may use an
equation %2x(t+1)_=_...%1 or sometimes %2x(t)_=_...%1.  This
formalism has two uses.

	First, Elephant provides a simple way of expressing sequential
programs as sentences in a first order theory which can then be used to
prove properties of the program.  This complements the first order
representation of recursive programs described in (Cartwright 1976) and
(Cartwright and McCarthy 1979) in that an Elephant program describes
what is to happen at successive times starting with the initial state,
while a recursive description describes how a desired function is
computed with the help its values for
simpler sets of arguments.  One might say
that Elephant is bottom-up while recursive programs are
top-down.

	Once a program has been expressed in Elephant, the %2inductive
assertion%1 and %2intermittent assertion%1 methods are automatically
available as particular techniques of making proofs within first order
logic.  They amount to using particular kinds of lemmas in proving
theorems.  Instances of the Hoare axioms are also just lemmas.

	The second aspect of Elephant (the
motivation for the name) is the ability to refer to the
whole past of the variables without specifying data structures for
remembering what has to be known in order to perform a current action.
Thus a reservation program written in Elephant can say that a passenger
has a reservation if he has made one and not cancelled it.  The program
needn't specify any data structure for remembering who has reservations;
%2an elephant never forgets%1.  Likewise, the rule that a castling
move is prohibited if the rook or king involved has ever moved is directly
expressible without inventing a variable to hold the information.

	Such reference to the past is certainly used in informal
English descriptions of what we want a computer to do.  Therefore, a
sufficiently high level programming language must have it.  On the other
hand, the Elephant programs that I have been able to write that refer
to the past are often more difficult to write and read than programs
with explicit data structures.  Perhaps I am simply inexperienced in
writing Elephant program, but most likely extensions to the formalism are
also needed.  Of course, there is no more reason to make a fetish out
not mentioning data structures than of not mentioning time.

	The simplest way to begin is with examples.
.skip 2
#. %3Expressing a sequential program in Elephant%1
.a←item
.a2←item

	Consider the following Algol 60 program fragment (declarations
omitted) for doing multiplication by iterated addition:

.begin nofill
%2

start:	i := n;				∂(30)0
	p := 0;				∂(30)1
loop:	qif i = 0 qthen qg done;	∂(30)2
	i := i - 1;			∂(30)3
	p := p + m;			∂(30)4
	qg loop;			∂(30)5
.end

One way of writing a corresponding Elephant program consists of the sentences

.begin nofill
.zz←12
%2

pc(0) =start,

∀t.[i(t+1) →=_∂(zz)IF pc(t) = start THEN n
∂(zz)ELSE IF pc(t) = start + 3 THEN i(t) - 1
∂(zz)ELSE IF start ≤ pc(t) ≤ start + 5 THEN i(t)
∂(zz)ELSE i(t+1)],

∀t.[p(t+1) →=_∂(zz)IF pc(t) = start + 1 THEN 0
∂(zz) ELSE IF pc(t) = start + 4 THEN p(t) + m
∂(zz)ELSE IF start ≤ pc(t) ≤ start + 5 THEN p(t)
∂(zz)ELSE p(t+1)],

%1and%2

∀t.[pc(t+1) →=_∂(zz)IF pc(t) = start + 2 ∧ i(t) = 0 THEN done
∂(zz)ELSE IF pc(t) = start + 5 THEN start + 2
∂(zz)ELSE IF start ≤ pc(t) ≤ start + 5 THEN pc(t+1)
∂(zz)ELSE pc(t+1].
.end

	In these equations ⊗i(t) and ⊗p(t) replace the
variables ⊗i and ⊗p of the Algol program.  The function ⊗pc(t) is the
program counter, and it takes values from %2start+1%1 to %2start+5%1
matching the numbers written on the right of the Algol program.  It is
be apparent from the example that any program made up of assignments
and qgs can be systematically translated to an Elephant program.
.if false then begin
We have used the logical conditional expression %2IF_..._THEN_..._ELSE%1
rather than qif_..._qthen_..._qelse, because there is no reason to
provide for an undefined case.  (The distinction is discussed in
(McCarthy and Talcott 1979)).
If the reader is a reactionary and
refuses to admit conditional expressions as terms in first order
logic, then they can be eliminated.  The equation for ⊗i(t+1) would
then split into the three cases

.begin nofill
%2

∀t.[pc(t) = 0 ⊃ i(t+1) = 0 ∧ pc(t) = 1 ⊃ i(t+1) = i(t) - 1
∂9∧ pc(t) ≠ 0 ∧ pc(t) ≠ 1 ⊃ i(t+1) = i(t)]
.end
.end

	Notice also that the length of the Elephant program is linear in the
length of the Algol program.

	Having one value of ⊗pc(t) for
each statement in the Algol program is unnecessary, although it makes
the systematic character of the translation more apparent.  If we
let %2pc(t)_=_start%1 correspond to the initialization and %2pc(t)_=_start+1%1
correspond to the loop, then the equations become

.begin nofill
.zz←12
%2

pc(0) = 0,

∀t.[i(t+1) →=_∂(zz)IF pc(t) = start THEN n
∂(zz)ELSE IF pc(t) = start+1 ∧ i(t) ≠ 0 THEN i(t) - 1
∂(zz)ELSE IF start ≤ pc(t) ≤ start+1 THEN i(t)
∂(zz)ELSE i(t+1)],

∀t.[p(t+1) →=_∂(zz)IF pc(t) = start THEN 0
∂(zz) ELSE IF pc(t) = start+1 ∧ i(t) ≠ 0 THEN p(t) + m
∂(zz)ELSE IF start ≤ pc(t) ≤ start+1 THEN p(t)
∂(zz)ELSE p(t+1)],

%1and%2

∀t.[pc(t+1) →=_∂(zz)IF pc(t) = start+1 THEN (IF i(t) = 0 THEN done ELSE start+1)
∂(zz)ELSE IF start ≤ pc(t) ≤ start+1 THEN pc(t) + 1
∂(zz)ELSE pc(t+1)].
.end

	That these programs compute the product of ⊗m and ⊗n is specified
by the sentence

	%2∃t.[pc(t) = done ∧ p(t) = m*n]%1.

It is provable from any first order axiomatization of arithmetic
together with the sentences constituting the program.  No special
axioms for programs or "logic of programs" is required.
One need only apply mathematical induction to the predicate

	%2qF(j) ≡ ∃t.(pc(t) = start+2 ∧ p(t) = m(n - i(t)) ∧ i(t) = j
⊃ ∃t.(pc(t) = done ∧ p(t) = mn)%1

The case %2j = 0%1 follows from the equation for ⊗pc(t+1), and the
induction step also follows from the Elephant program.  The desired
result is the conclusion of %2qF(n)%1, and the premiss
of %2qF(n)%1 follows from the initial conditions.

	Thus an entirely conventional mathematical way of writing
recursion equations leads to a convenient programming language.  It
is tempting to call the language Algol 50, since it only uses ideas that
were familiar in 1950.

	The proof of correctness for this
multiplication program is misleadingly simple, since
we can easily write explicit formulas for ⊗i(t), ⊗p(t), and
⊗pc(t) and prove them by mathematical induction.  More typical proofs
occur when it isn't convenient to give explicit formulas for the
variables as functions of time or for the value of ⊗t for which the
program terminates.  Then the computational content of the proof is
is often essentially the same as that of an %2inductive assertions%1 proof
combined with induction on a rank function of the variables taking
values in a suitable inductively ordered set.

.skip 3
#. %3Reversing a list%1

	Reversing a list provides another example of an Elephant program
that can be compared with a recursive conditional expression program
for the same function.  We start with a Lisp "program feature" program
written in the style of Algol 60.
.begin nofill
%2
.z←8

∂zu := w;
∂zv := qNIL;
∂1loop:	∂zqif null u qthen qg done;
∂zv := [qa u] . v;
∂zu := qd u;
∂zqg loop;
∂1done:

.end

	The corresponding Elephant program is

.begin nofill
%2
.zz←12

pc(0) = 0,

∀t.[u(t+1) →=_∂(zz)IF pc(t) = 0 THEN w
		∂(zz)ELSE IF pc(t) = 1 ∧ ¬null u(t) THEN qd u(t)
		∂(zz)ELSE u(t)],

∀t.[v(t+1) →=_∂(zz)IF pc(t) = 0 THEN qNIL
		∂(zz) ELSE IF pc(t) = 1 ∧ ¬null u(t) THEN qa u(t) . v(t)
		∂(zz) ELSE v(t)]

∀t.[pc(t+1) →=_∂(zz)IF pc(t) = 1 ∧ ¬null u(t) THEN 1
		∂(zz)ELSE pc(t) + 1].
.end

	This can be compared with the LISP program ⊗reverse defined by

	%2reverse u ← qif qn u qthen qNIL qelse reverse qd u * <qa u>%1.

With the latter, as shown in (Cartwright and McCarthy 1979), it is
convenient to prove such properties as %2reverse_reverse_u_=_u%1 and
%2reverse[u_*_v]_=_reverse_v_*_reverse_u%1.  The major fact about
the Elephant program is expressed by

	%2∃t.(pc(t) = 2 ∧ v(t) = reverse w)%1.

It can be proved by proving that %2length u(t)%1 is a decreasing function
of ⊗t, i.e. for any ⊗t such that ⊗pc(t)_<_2, there is %2t'_>_t%1 such
that %2length_u(t')_<_length_t%1, and also that

	%2∀t.[reverse_w = reverse u(t) * v(t)]%1.

This is just another %2inductive assertions%1 proof.  So far it seems that
the most convenient technique for proving facts about Elephant programs
is %2inductive assertions%1,
which is less flexible than the technique described in (Cartwright and
McCarthy 1979) that uses the %2functional equation%1 and the %2minimization
schema%1.  This is because %2inductive assertions%1 provides no way
of expressing algebraic relations among functions defined by programs.

	One mathematically straightforward way of defining functions by
programs is the following.  We rewrite the above equations to introduce
⊗w as an explicit argument of the functions so that they become ⊗u(t,w), 
⊗v(t,w), and pc(t,w).  We then define a relation ⊗reverses(v,w) by

	%2∀v w.(reverses(v,w) ≡ ∃t.(pc(t,w) = 2 ∧ v(t,w) = v))%1.

When we have proved %2∀w ∃!v.reverses(v,w)%1, first order logic
entitles us to replace the relation ⊗reverses by a function.  We can
then prove successively that this function satisfies the relations

	%2reverse qNIL = qNIL%1,

	%2reverse [x . u] = reverse u * <x>%1

	%2reverse reverse u = u%1,

and

	%2reverse[u * v] = reverse v * reverese u%1,

where the notation is as in (McCarthy and Talcott 1979).

.skip 3
#. %3Another Elephant Formalism%1

	The Elephant formalism of the previous sections sorts the program
by variables, while a sequential program sorts it according to the program
counter.  The latter is more conventional and often more convenient.
Moreover, if we want to represent pieces of program separately and
combine them by taking conjunctions, sorting by program counter seems
to work better.

	Our pc-sorted Elephant involves three changes:

	1. Instead of writing ⊗x(t), we write ⊗value(x,t).  This allows
us to quantify over variables and is useful for combining the qelse
cases.

	2. Instead of starting the program counter at 0, we give each
program a symbolic entry location.  This is analogous to the machine
language idea of a relocatable program, and it has the same use.
It enables us to combine programs by conjunction, and we can suppose
that numerical values of the entry locations of the parts of the
program are specified so that no distinct parts of the programs have
the same values of the program counter.  Indeed
specifying the values of the entry locations in a way that corresponds
to overlapping programs will usually lead to a contradiction in
the combined sentence.

	3. We have one equation that specifies ⊗value(var,t+1)).  Its right
side is a conditional expression whose clauses correspond to the
different values of the program counter.

	With all these changes, our program ⊗P1 for multiplication by
addition is

.begin nofill
.zz←12

%2
∀var t.[value(var,t+1) =
∂(zz)IF value(pc,t) = entry1 ∧ var = i THEN n
∂(zz)ELSE IF value(pc,t) = entry1 + 1 ∧ var = p THEN 0
∂(zz)ELSE IF value(pc,t) = entry1 + 2 ∧ var = pc ∧ value(i,t) = 0 THEN exit1
∂(zz)ELSE IF value(pc,t) = entry1 + 3 ∧ var = i THEN value(i,t) - 1
∂(zz)ELSE IF value(pc,t) = entry1 + 4 ∧ var = p THEN value(p,t) + 1
∂(zz)ELSE IF value(pc,t) = entry1 + 5 ∧ var = pc THEN entry1 + 2

∂(zz)ELSE IF entry1 ≤ value(pc,t) ≤ entry1 + 5 ∧ var = pc THEN value(pc,t) + 1
∂(zz)ELSE IF entry1 ≤ value(pc,t) ≤ entry1 + 5 THEN value(var,t)
∂(zz)ELSE value(var,t+1)%1

.end

	Notice that there is one clause for each statement in the Algol
program and three additional clauses.  The first additional clause states that
the program counter is increased by 1 within the program unless something
else is previously stated about that value
of the program counter.  The second states that variables
whose behavior is not previously specified in the program retain their
values within the program segment.  The last clause manages, by being
tautologous, to say nothing about what happens outside of the range
%2entry1_≤_pc_≤_entry1+5%1, thus avoiding interference with sentences
specifiying other programs that might be combined with ⊗P1. 

	Indeed suppose ⊗P2 is another program involving some of the same
same variables as ⊗P1 and possibly some others, and suppose we
want to combine these programs so that ⊗P2 is executed after ⊗P1.
We need only take the conjunction of the sentences together with
the sentence %2entry2_=_exit1%1.  Should we want to do so, we
can transform the conjunction into an equivalent sentence which
has the same form as ⊗P1 or ⊗P2, i.e. a clause for each statement
and three clauses at the end.

	Combination by conjunction works the same
in more complicated cases.  A program can have multiple entries
and exits, any exit can be connected to any entry just by equating
suitable ⊗entry and ⊗exit parameters.
.if true then begin "defining functions"
.skip 2
#. %3Defining Functions in Elephant%1

	Work in program verification has most often concerned itself
with verifying input-output relations of programs, and the previous
section shows how to do this for Elephant programs.  Indeed
 some authors
have left their readers with the impression that this is all there is
to program verification.

	There is also proving equivalence of progams in various senses
and proving properties of functions computed by programs.  In order to
prove properties of functions computed by Elephant programs, we
proceed as follows:

	Given a relation ⊗P(x,y), we can partially define a function ⊗f by

!!w1:	%2∀x.(∃y.P(x,y) ⊃ P(x,f(x)))%1

provided ⊗f is a fresh function symbol.  No contradiction arises from
({eq w1}), because if there isn't any ⊗y such that ⊗P(x,y), then ⊗f(x) is
entirely unrestricted.  Therefore, nothing need be proved to entitle
us to write ({eq w1}).  However, if ⊗∀x∃!y.P(x,y) holds, then ⊗f is
completely determined, and ({eq w1}) can be used to prove its properties.

	We can use this idea in the Elephant context to write

!!w2:	%2∀x.(∃t.(pc(t,x) = done ∧ ∀t'(t' < t ⊃ pc(t') ≠ done))
⊃ pc(qt(x),x) = done ∧ ∀t'.(t' < qt(x) ⊃ pc(t') ≠ done))%1

thus partially defining a function qt, which gives the time
at which the program terminates as a function
of the input parameter ⊗x.  If we want ⊗f(x)
to be the value of the variable ⊗y when the programs gets to ⊗done, we
then write

!!w3:	%2∀x.(f(x) = y(qt(x),x))%1.

We can then use ({eq w2}) and ({eq w3}) to prove any desired properties
of ⊗f.  Some of these properties, including algebraic relations like
associativity are not directly expressible as input-output relations
of the program.
.end "defining functions"
.skip 2
#. %3Equivalence of Elephant programs%1

.begin
.turn on "↓"
.at "uu" ⊂"%3u%*"⊃
.at "vv" ⊂"%3v%*"⊃
.at "xx" ⊂"%3x%*"⊃
.at "yy" ⊂"%3y%*"⊃


	Definitions of the equivalence of Elephant programs,
equivalence-preserving transformations of programs, and techniques for
proving equivalence can be expected to be important in applications.
Indeed one approach to compiling is to transform a general
Elephant program into an immediate program using equivalence-preserving
transformations.

	Equivalence relations should be defined that will facilitate
such processes.  An obvious form of equivalence is to require that each
variable in the two programs be represented by the same function of
time for all values of the parameters.  This is too strict an equivalence
to be interesting on two grounds.  First, the two forms of the multiplication
by addition program in section {a2} would not be equivalent, because
one of them goes around the loop in one time step while the other takes
four steps.  Second, transforming a program to an immediate program may
involve the introduction of new variables, arrays and other data structures
in order to eliminate the direct references to the past.

	In fact many kinds of equivalence are useful.
We begin with a class of equivalence relations based on a notion of
an equivalence between states of two programs.  However, we don't want
to assume that every state of each program has a corresponding state
in the other; only certain states will correspond.  We certainly want
the beginning and ending states to correspond, and we also want to be
sure that any state of one program that corresponds to another will
eventually be followed by a state that should also correspond.  Here is
how these ideas can be formalized.

	Let one Elephant program ⊗P have functions ⊗u↓1(t),_..._,u↓m(t) and
a second ⊗P' have functions ⊗u↓1'(t)_..._u↓n'(t).  To avoid prolixity,
we summarize these functions as vectors %2uu(t)%1 and %2uu'(t)%1.  Let
%2EV(uu,uu')%1 be a relation.  Let ⊗P depend on
parameters %2x↓1,_..._x↓p%1 and ⊗P' have parameters %2x↓1'_..._x↓q'%1,
similarly summarized into vectors %2xx%1 and %2xx'%1.
(The parameters of the program for multiplication by addition were ⊗m and ⊗n). 
Let %2EP(xx,xx')%1 be a relation between the parameter vectors.
Also let %2Q(uu)%1 and %2Q'(uu')%1 be predicates that say what states of the
two programs are to be compared.
Now suppose we can prove that

	%2P ∧ P' ∧ EP(xx,xx') ⊃ EV(uu(0),uu'(0)) ∧ Q(uu(0)) ∧ Q'(uu'(0))%1,

i.e. that the initial states of the programs are comparable and correspond,
and

	%2P ∧ P' ⊃ ∀t1 t2 t1'.[EV(uu(t1),uu'(t1')) ∧ t2 >t1 ∧ Q(uu(t2))
 ⊃ ∃t2'.EV(uu(t2),uu'(t2'))]%1,

i.e. that any comparable state of ⊗P that corresponds to a state of ⊗P'
is followed by another comparable state that corresponds to a state of ⊗P', 

and going the other way

	%2P ∧ P' ⊃ ∀t1 t1' t2'.[EV(uu(t1),uu'(t1')) ∧ t2' >t1' ∧ Q'(uu'(t2'))
 ⊃ ∃t2.EV(uu(t2),uu'(t2'))]%1.

We should then call the programs ⊗P and ⊗P' equivalent with respect
to the the conditions ⊗Q and ⊗Q' and the relations ⊗EP and ⊗EV. 
Note that we have used the programs themselves as hypotheses since we can
regard a program as the conjunction of its constituent sentences.

	The two versions of multiplication by addition are equivalent
with respect to the predicates

	%2EP(m,n,m',n') ≡ m=m' ∧ n=n'%1,

	%2Q(i,p,pc) ≡ pc = 2 ∨ pc = done%1,

	%2Q'(i',p',pc') ≡ pc' = 1 ∨ pc' = done%1,

and

	%2EV(i,p,pc,i',p',pc') ≡ (pc=0 ∧ pc'=0) ∨
[i=i' ∧ p=p' ∧ (pc=2 ∧ pc'=1 ∨ pc=6 ∧ pc'=2)]%1

They should be sufficient to prove that one program is correct (according
to the definitions of section {a2}) if and only if the other is.
.end


#. %3Non Immediate Elephant Programs%1

	When we translate an Algol program into Elephant, we get
equations in which the %2x(t+1)%1s depend only on the %2x(t)%1s.
We will call such a program an %2immediate%1 Elephant program.
However, the recursion
equations will still have guaranteed solutions if the %2x(t)%1s depend on
arbitrary earlier values of ⊗t.  This leads to a "high level" programming
language with the following features:

	1. The program refers to the past through earlier values of
⊗t, just as though everything were remembered.

	2. The compiler is smart and decides what data structures are
required in order to carry out the computations without remembering
everything.  To the extent that compilers can be written that do this
effectively, Elephant is a "higher level" language in which the
programer specifies less than in Algol, etc.

.skip 2
#. %3An airline reservation system%1

	Consider programming a trivial airline reservation system.
We want to say that %2a passenger has a reservation if he
has made one that has not been cancelled%1.  We do not want to prescribe
what data structures have to be kept in order to be able to answer the
question of whether someone has a reservation.

	This program replies properly to requests to make reservations,
cancel them, and to inquiries about whether a reservation exists.
The program refers to its input in
terms of an abstract analytic syntax the meaning of whose mnemonic
predicate and function names is hopefully obvious.  The only data
structure explicitly mentioned is the number of seats currently occupied,
and even that could be eliminated from the program.  The Elephant compiler,
therefore, gets the honor of determining what other data structures
are needed.  We use the convention of writing %2α{xα}f%1 instead of ⊗f(x) when
it is convenient to write the argument before the function name.
.begin nofill
.uu←35
%2

∀t.[output(t+1) = α{input(t)α}[λ in.
∂(10)IF ismake in THEN →[∂(uu)IF hasrev(maker in,t) THEN "You had it"
			∂(uu)ELSE IF number(t) = N THEN "No room"
			∂(uu)ELSE "You have it now"]
∂(10)ELSE IF iscancel in THEN →[∂(uu)IF hasrev(maker in,t) THEN "It's cancelled"
			∂(uu)ELSE "You don't have it to cancel"]
∂(10)ELSE IF isinquiry in THEN→[∂(uu)IF hasrev(maker in,t) THEN "You have one"
			∂(uu)ELSE "You don't have one"]
∂(10)ELSE qNIL]

∀t.[number(t+1) = α{input(t)α}[λ in.
∂(10)IF ismake in THEN →[∂(uu)IF hasrev(maker in,t) ∨ number(t) = N
∂(uu)THEN number(t)
∂(uu)ELSE number(t) + 1]
∂(10)ELSE IF iscancel in THEN →[∂(uu)IF hasrev(maker in,t) THEN number(t) - 1
			∂(uu)ELSE number(t)]
∂(10)ELSE number(t)]
.end

where

	%2∀t.[hasrev(passenger,t) ≡ ∃t1.(t1 < t ∧ ismake input t1 ∧
passenger = maker input t1 ∧ number(t1) < N) ∧ ¬∃t2.(t1 < t2 < t ∧
iscancel input t2 ∧ maker input t2 = passenger))]%1.

	The main difficulty in making a compiler for Elephant is illustrated
by the predicate ⊗hasrev.  The compiler has to understand that it
must remember successful reservations but can forget unsuccessful
attempts at making a reservation and that it can forget reservations
that have been cancelled.  Perhaps ⊗hasrev should be written using primitives
that refer explicitly to the most recent occurrence of an event,
which might permit a less intelligent compiler.

.if false then begin
#. Elephant program to count vertices in a list structure

.begin nofill
****
There seems to be a bug in this program and the %2samefringe%1 program
that we hope to fix in a subsequent draft.
****
.end

	Another context in which it is possible to avoid specifying a
data structure by referring to the past, occurs when a list structure
is to be scanned.  The simplest example is a program to count the
vertices in a list structure.

Here ⊗a is the list structure being scanned, ⊗x is a running variable for
the current structure, and ⊗n is the current count.

	Because of Elephant's ability to refer to the past, we can
write this program without specifying a stack.  It is up to the compiler
to decide that a stack is appropriate for implementing the algorithm.

.begin nofill
%2 

∀t.[x(t+1) →=_∂(16)IF pc(t) =_0 THEN a
∂(16)ELSE IF pc(t) =_1 THEN
→[∂(22)IF [∀y.seen(y,t) ⊃ atom y ∨ seen(car y,t) ∧ seen(cdr y, t)]
∂(30)THEN x(t)
∂(22)ELSE IF ¬atom x(t) ∧ ¬seen(car x(t),t) then car x(t)
∂(22)ELSE cdr x(mostrecent(t,λt1.¬seen(cdr(x(t1)),t)))]
∂(16)ELSE x(t)]

∀t.[n(t+1) →=_∂(16)IF pc(t) =_0 THEN 0
∂(16)ELSE IF ∂(25)pc(t) =_1 
→∧ ∂(25)¬[∀y.seen(y,t) ⊃ atom y ∨ seen(car y,t) ∧ seen(cdr y, t)]
∂(30)THEN n(t) + 1
∂(16)ELSE n(t)]

∀t.[pc(t+1) →=_∂(16)IF ∂(20)pc(t) =_1
→∧ ∂(20)¬[∀y.seen(y,t) ⊃ atom y ∨ seen(car y,t) ∧ seen(cdr y, t)]
∂(25)THEN 1
∂(16)ELSE pc(t) + 1
.end

where the predicate ⊗seen and the functional ⊗mostrecent are defined as
follows:
.begin nofill
%2 

∀y t.[seen(y,t) ≡ ∃t1.[t1 ≤ t ∧ y =_x(t1)]]

∀t.[mostrecent(t, pred) = qif pred t qthen t qelse mostrecent(t - 1, pred)].
.end

We would like to regard these as definitions not as programs.  Indeed the
compiled program shouldn't compile them directly, but should do the job
another way that uses time and space more efficiently.

Of course, this example is less perspicuous than the Lisp program

%2count x ← qif qat x qthen 1 qelse count qa x + count qd x%1

which scans the vertices in the same order.  But then this problem
is especially appropriate for recursion and Lisp's built-in stack
mechanism.

Most likely ⊗seen and ⊗mostrecent will occur in other algorithms
where one doesn't want to look at things that have been already tried.

#. %2samefringe%1

	The LISP predicate %2samefringe[x,y]%1 may be defined by

%2samefringe[x1,x2] ≡ fringe x1 = fringe x2%1,

where %2fringe_x%1 is a list of the atoms in ⊗x and is defined by

%2fringe x ← qif qat x qthen <x> qelse fringe qa x . fringe qd x%1.

	The above definition does not provide the most efficient
computation of ⊗samefringe, and a better LISP function is given
in (Cartwright and McCarthy 1979), and a proof of its correctness
is outlined.  A detailed computer-checked proof is given in
(Talcott 1979).

	The following is an Elephant program for %2samefringe%1.

.begin nofill
%2
.a←12;b←28;c←35;

pc(0) = 0

∀t.[x1(t+1) →=_∂aIF pc(t) = 0 THEN x1
∂aELSE IF pc(t) = 1 THEN
→[∂bIF [∃y.seen1(y,t) ∧ ¬atom y ∧ [¬seen1(car y,t) ∨ ¬seen1(cdr y,t)]
∂cTHEN cdr x1(mostrecent(t,λt1.¬seen1(cdr(x1(t1)),t)))
∂bELSE x1(t)]
∂aELSE IF pc(t) = 2 THEN
→[∂bIF [∃y.seen1(y,t) ∧ ¬atom y ∧ [¬seen1(car y,t) ∨ ¬seen1(cdr y,t)]
∂cTHEN cdr x1(mostrecent(t,λt1.¬seen1(cdr(x1(t1)),t)))
∂b ELSE IF ¬atom x1(t) THEN car x1(t)
∂b ELSE x1(t)]
∂a ELSE x1(t)]

∀t.[x2(t+1) →=_∂aIF pc(t) = 0 THEN x2
∂aELSE IF pc(t) = 1 THEN
→[∂bIF [∃y.seen2(y,t) ∧ ¬atom y ∧ [¬seen2(car y,t) ∨ ¬seen2(cdr y,t)]
∂cTHEN cdr x2(mostrecent(t,λt1.¬seen2(cdr(x2(t1)),t)))
∂bELSE x2(t)]
∂aELSE IF pc(t) = 2 THEN
→[∂bIF [∃y.seen2(y,t) ∧ ¬atom y ∧ [¬seen2(car y,t) ∨ ¬seen2(cdr y,t)]
∂cTHEN cdr x2(mostrecent(t,λt1.¬seen2(cdr(x2(t1)),t)))
∂b ELSE IF ¬atom x2(t) THEN car x2(t)
∂b ELSE x2(t)]
∂a ELSE x2(t)]

∀t.[pc(t+1) →=_∂aIF (pc(t) = 1 ∨ pc(t) = 2 ∧ atom x1(t) ∧ atom x2(t) ∧ x1(t) ≠ x2(t)
∂bTHEN 4
∂aELSE IF pc(t) = 2 ∧ atom x1(t) ∧ atom x2(t) THEN 1
∂aELSE IF ∂bpc(t) = 1
→∧_∂b∀y.[seen1(y,t) ⊃ atom y ∨ seen1(car y,t) ∧ seen1(cdr y,t)]
→∧_∂b∀y.[seen2(y,t) ⊃ atom y ∨ seen2(car y,t) ∧ seen2(cdr y,t)]
∂cTHEN 5
∂aELSE IF ∂bpc(t) = 1
→∧_[∂b∀y.[seen1(y,t) ⊃ atom y ∨ seen1(car y,t) ∧ seen1(cdr y,t)]
→∨_∂b∀y.[seen2(y,t) ⊃ atom y ∨ seen2(car y,t) ∧ seen2(cdr y,t)]]
∂cTHEN 4
∂a ELSE pc(t) + 1]

%1where%2

∀y t.[seen1(y,t) ≡ ∃t1.[t1 ≤ t ∧ y =_x1(t1)]]

%1and%2

∀y t.[seen2(y,t) ≡ ∃t1.[t1 ≤ t ∧ y =_x2(t1)]].

.end

	As Thurber might have put it, compared to the recursive definition,
this is a little big and pretty ugly.  However, it does have a certain
brute force straightforward character, and it certainly leaves to the
compiler the task of inventing suitable data structures.

	The theorem to be proved is

%2(samefringe(x1,x2) ≡ ∃t.(pc(t) = 5)) ∧ (¬samefringe(x1,x2) ≡ ∃t.(pc(t) = 4))%1.
.end

.<<dining philosophers>>
.if false then begin 

	1. Francez's proof readily translates into a formal elephant
proof, and it may be worthwhile to do the translation.


	2. N(t1,t2) can be taken as the number of philosophers who
have expressed a desire to eat at time t1 but still haven't eaten
by t2.  We can define a quantity which we intend to have that
interpretation, but we don't have to prove it.  We only have to
prove that it will be positive if a philosopher who wants to eat
at time t1 hasn't eaten by t2  and that if it is zero, then all
philosophers who wanted to eat at t1 have indeed eaten by t2.

On the other hand, there may be some reason to define the quantity
set theoretically as

	N(t1,t2) = card α{x ε philosophers|R(x,t1) = eat ∧ ∀t'.(t1≤t'≤t2
⊃ ¬S(x,t')=eatα}

	If we suppose that a philosopher may change his mind about
eating, then we need only guarantee to feed those who persist in their
desire to eat, so that

	N(t1,t2) = card α{x ε philosophers|R(x,t1) = eat ∧ ∀t'.(t1≤t'≤t2
⊃ R(x,t')=eat ∧ ¬S(x,t')=eatα}

The correctness of the program is then expressed by

	∀t1 ∃t2.N(t1,t2) = 0

A natural way to proceed would be to define an ordinal function of time,
αα(t1,t2), such that N(t1,t2) is the coefficient oof some power of
omega and the lower order terms measure progress through the program.
Then we would prove that unless αα(t1,t) is zero, it decreases with
each time step.  However, we seem to be frustrated by the fact that
our condition on stopping eating is simply that an eater will eventuall
stop; we don't have a bound on the time he will take, and it may
well depend on our strategy.  For example, an eater may dislike one
of his neighbors and decide to eat as long as possible if that neighbor
wants to eat.  How long he can eat may depend on his ability to sneak
food onto the floor with the help of this other neighbor.  We only
have the guarantee that he won't keep it up indefinitely.

	This proof strategy will work for Francez's proof of the
correctness of Dijkstra's garbage collector.  Here N(t1,t2) is defined
to be the number of nodes that are inaccessible at t1 and uncollected
by t2.  We should be ablee to prove that a certain ordinal function
that we can write down is always decreasing.  Moreover, the proof
should be a single simplification step.  Almost all the required
ingenuity has been applied in designing the garbage collection
algorithm.  This idea has ssome ope of trivializing most program
proving.
.end
#. %3Parallel processes for computing a sum of functions%1

.begin
.turn on "[]↑↓&"
.font B "BDJ20"

	The following Elephant program computes %AS%B↑N&↓[n=1]%2f(n))%1
using ⊗k processors.  A master processor with program counter ⊗pc(t) 
initializes the variables ⊗n and ⊗s and starts the ⊗k slave
processes whose program counters are written ⊗pc(i,t) 
at step 1.  A process needs exclusive access to ⊗n when
reading and incrementing it, need exclusive access
to ⊗s when incrementing it, and we only provide for exclusive access
at these times.  We presuppose that computing ⊗f(n) takes ⊗time(n) units
of time, and these operations are done in parallel.  ⊗pc(t) is the
program counter for the master process, and ⊗pc(i,t) is the program
counter of the %2i%1th slave process.  The updating of all variables
except the ⊗pc(i,t) works as in Algolic programs, but the latter
requires a more elaborate and somewhat implicit description that may
well challenge the designer of an Elephant compiler.
.end

.begin nofill
.ww←10
%2 

n(t+1)→=_∂(ww)IF pc(t) = 0 THEN 1
∂(ww)ELSE IF pc(i,t) = 1 ∧ n(t) ≤ N THEN n(t) + 1
∂(ww)ELSE n(t)

s(t+1)→=_∂(ww)IF pc(t) = 0 THEN 0
∂(ww)ELSE IF pc(i,t) = 5 THEN s(t) + m(i,t)
∂(ww)ELSE s(t)

m(i,t+1)→=_∂(ww)IF pc(i,t) = 3 ∧ n(t) ≤ N THEN n(t)
∂(ww)ELSE IF pc(i,t+1) = 4 THEN f(m(i,t))
∂(ww)ELSE m(i,t)

pc(t+1) →=_∂(ww)IF pc(t) = 1 ∧ ∃i.(pc(i,t) ≠ 0) THEN 1
∂(ww)ELSE pc(t) + 1


pc(i,0) = 0

pc(i,t) = 0 ⊃ pc(i,t+1) = IF pc(t) = 0 THEN 1 ELSE 0

pc(i,t) = 1 ⊃ ∃!j.(pc(j,t) = 1 ∧ pc(j,t+1) = 2) ∧ ∃t'.(t < t' ≤ t+k ∧ pc(i,t') = 2)

pc(i,t) = 1 ⊃ pc(i,t+1) = 1 ∨ pc(i,t+1) = 2

pc(i,t) = 2 ⊃ pc(i,t+1) = IF n(t) ≤ N THEN 3 ELSE 0

pc(i,t) = 3 ∧ pc(i,t-1) ≠ 3 
∂(ww)⊃ ∀t'.(t ≤ t' < t + time(m(i,t)) ⊃ pc(i,t') = 3) ∧ pc(t+time(m(i,t))) = 4

pc(i,t) = 4 ⊃ ∃!j.(pc(j,t) = 4 ∧ pc(j,t+1) = 5) ∧ ∃t'.(t < t' ≤ t + k ∧ pc(i,t') = 5)

pc(i,t) = 5 ⊃ pc(i,t+1) = 1
.end

	It may be questioned whether the above Elephant program should be
regarded as a "program" that can be compiled by a suitable compiler or as
something between a specification and a program.  Perhaps it is an example
of that elusive concept called an algorithm.  Notice that it assumes that
synchronization occurs without specifying any way of doing it.  Just the
thing to challenge a smart compiler or automatic programming system.  On
the other hand, the correctness of the Elephant program is given by the
statement,

.begin nofill
.turn on "[]↑↓&"
.font B "BDJ20"

%2∃t.(pc(t) = 2 ∧ ∀i(pc(i,t) = 0) ∧ s(t) = %AS%B↑N&↓[n=1]%2f(n))%1
.end

and this can presumably be proved from the program.  The correspondence
between this Elephant program and one that is more explicit about
synchronization might be proved separately.

	There may well be better ways of describing parallel processes
in Elephant.

.skip 2
#. %3Temporal Logic Considered Unnecessary%1

α{t| P(tα}

x is increasing with time

P is true until the first time Q is true

Relations between values of the variables at different times
can be expressed in temporal logic but only with extra quantifiers.

	The Elephant approach to representing programs and proving
their properties is a close relative of the modal logic approach
of (Pnueli 1978) and (Manna and Pnueli 1979).  Their formalism
also explicitly refers to the values of the program counter but
treats it in formally different way from ordinary program variables.
However, instead of representing variables as functions of time,
they use temporal operators ⊗F (eventually), ⊗G (for all future
times) and ⊗X (at the next time).  (This is Pnueli's notation, the
joint paper uses the qD, qN common in modal logic together with
qO for ⊗X).

	The modal logic is justified in (Manna and Pnueli 1979) as follows:

	%2"In spite of these qualifications there are some obvious advantages
in the introduction and use of modal formalisms.  It allows an
explicit discrimination of one parameter as being appreciably more
significant than all the others, and makes dependence on that parameter
implicit.  Nowadays, when increasing attention is paid to the clear
correspondence between syntax and natural reasoning (as is repeatedly
stressed by the discipline of Structured Programming), it seems only
appropriate to introduce extra structure into the description of
varying situations.  Thus a clear distinction is made between variation
within a state, which we express using predicates and quantifiers,
and variation from one state to another, which we express using modal
operators"%1.

	Manna and Pnueli are right in asserting that in programming
variation in time is especially significant.  Unfortunately, expressing
temporal variation
with modal operators makes time a second class citizen and limits
what can be conveniently said about it.
Let us compare some Elephant assertions with the corresponding
assertions in temporal logic.

1. Total correctness of a program

	%2∀t qF(x(t)) ⊃ ∃t'.(t' > t ∧ pc(t') = done ∧ qP(x(t),x(t'))%1

	%2qF(x) ∧ x = a ⊃ F [at done ∧ qP(a,x)]%1

2. Partial correctness of a program

	%2∀t t'.

The following examples taken from (Manna and Pnueli 1979) 
Kamp defined two tenses by the equivalences:

p S q ≡ (∃t)α{t < n ∧ q(t) ∧ (∀t')[t < t' < n) ⊃ p(t')]α}

p T q ≡ (∃t)α{n < t ∧ q(t) ∧ (∀t')[n < t' < t) ⊃ p(t')]α}

Here %2p S q%1 is read "⊗p since ⊗q ", and %2p T q%1 is read "⊗p till ⊗q ". 
Kamp (1968) proved that for dense time, infinite in both directions,
⊗S and ⊗T are not definable in terms of any unary tenses and
that all "tenses" can be defined in terms of ⊗S and ⊗T.   While this
doesn't show that ⊗S and ⊗T can't be defined in terms of unary
tenses for integer time, I'll be they can't.  Moreover, ⊗T would
seem to be an entirely relevant tense for proramming.  It says that
⊗p will be true until ⊗q becomes true.

.skip 2
#. %3Remarks%1

1. Programs in Lucid (Ashcroft and Wadge 1976) are also collections of sentences 
in a first order language.  A Lucid object is a vector of the values 
of a variable throughout time.  This permits some statements to be
made in a very neat way.  However, it seems to be less flexible than
the Elephant device of admitting the time as an explicit parameter.
Lucid programs do not admit qgs, and there are other unexpected
restrictions.  Perhaps some of Lucid's problems would be cured by
including the history of the program counter as a variable.

2. The properties of Elephant programs don't depend on time taking
integer values.  All we need require is that the set of times be ordered
and unbounded above.  Then the first sentence of the product program
would take the form
.begin nofill
.u←20

%2∀t ∃t'.[t' > t ∧ i(t') →=_∂uIF pc(t) = 0 THEN n
∂uELSE IF pc(t) = 3 THEN i(t) - 1
∂uELSE i(t)].
.end

3. It seems to me that any language that purports to allow the user to say
what he wants the computer to do in English, should allow the executive or
general or other big shot to say that %2a customer has a reservation if he
has made one and it hasn't been cancelled%1.  The big shot certainly
doesn't want to concern himself with what data structures are required in
order to fulfill his wishes, and Elephant shows that his wishes can be
stated without mentioning such a data structure.

4. In its present state, Elephant doesn't seem to be a very easy
language to use.  I say "seem", because the awkward programs may
be merely a consequence of inexperience.  Of course, Algolic programs
can easily be translated into Elephant, but this doesn't take
advantage of Elephant's ability to refer directly to the past.

5. Regarded simply as a way of writing Algolic programs as logical
sentences, Elephant plays a role similar to that played by the Cartwright
way of writing Lisp style recursive conditional expression programs as
logical sentences.  In fact it may be a kind of dual to the Cartwright
method just as %2inductive assertions%1 and %2subgoal induction%1 seem to
be duals.  Namely, Elephant programs and inductive assertions work from an
initial state and describe its changes, while Lisp style programs and
subgoal induction work backwards from desired final result.  Thus it may
complete a pattern of methods of program formalization.

6. Elephant may be expanded by relaxing the restriction that statements
refer only to the past.  Our big shot may wish to say, %2"When the
passengers arrive at the airport for the flight, an airplane and a crew
will have been summoned by the scheduling program to fly them to their
destination"%1.  Allowing the right hand sides of Elephant equations to
refer to the future puts a heavier burden on the compiler.  In fact, many
futuristic Elephant program are contradictory and hence uncompilable.
Thus a compiler for futuristic Elephant is really a kind of problem
solver.  Nevertheless, this style of programming may prove practicaly
useful and theoretically illuminating.

8. Church (1957) represents digital circuits as recursive systems of Boolean
equations determining the behavior of a collection of Boolean
variables as a function of time.  He discusses the synthesis of circuits
with given behavior.  Some of his results might lead to theorems
about classes of Elephant programs over finite domains in cases where
the finiteness of the domain is important.
.skip 2
#. %3References%1

%3Ashcroft, E. A. and W. W. Wadge (1976)%1: Lucid - A Formal System
for Writing and Proving Programs, %2SIAM Journal of Computing%1,
Vol. 5, No. 3, September.

%3Burgess, John P. (1979)%1: "Logic and Time", %2Journal of Symbolic
Logic%1, vol. 44, No. 4, Dec. 1979.

%3Cartwright, R.S. (1976)%1:
%2A Practical Formal Semantic Definition and Verification System
for Typed Lisp%1,
Ph.D. Thesis, Computer Science Department, Stanford University,
Stanford, California.

%3Cartwright, Robert and John McCarthy (1979)%1: "Recursive Programs
as Functions in a First Order Theory", in E. Blum and S. Takasu (eds.),
%2Proceedings of the International
Conference on Mathematical Studies of Information Processing%1, Springer
Publishers.

%3Church, Alonzo (1957)%1: "Application of Recursive Arithmetic to the
Problem of Circuit Synthesis", in %2Summaries of talks presented at the
Summer Institute for Symbolic Logic, Cornell University 1957%1.,
Institute for Defense Analyses.

%3Francez, Nissim and Amir Pnueli (1978)%1: "A Proof Method for Cyclic
Programs", %2Acta Informatica%1 9, 133-157.

%3Francez, Nissim (1976)%1: %2The Analysis of Cyclic Programs%1, PhD
Thesis, Weizmann Institute of Science, Rehovot, Israel.

%3Francez, Nissim (1978)%1: "An Application of a Method for
Analysis of Cyclic Programs", %2IEEE Transactions on Software
Engineering%1, vol. SE-4, No. 5, pp. 371-378, September 1978.

%3Kamp, Hans (1968)%1: %2On Tense Logic and the Theory of Order%1,
PhD Thesis, U.C.L.A.

%3Kroger, F. (1978)%1: "A Uniform Logical Basis for the Description,
Specification and Verification of Programs", in E.J. Neuhold (ed.),

%3Manna, Zohar and Amir Pnueli (1979)%1: %2The Modal Logic of Programs%1,
preliminary version of technical report, Computer Science Department,
Stanford University.
%2Formal Descriptions of Programming Concepts%1, North-Holland.

%3McCarthy, John and Carolyn Talcott (1980)%1: 
%2LISP: Programming and Proving%1,
(in preparation)

%3Pnueli, A. (1978)%1: %2The Temporal Semantics of Concurrent Programs%1,
Technical Report, Tel-Aviv University.

%3Prior, A. N. (1967)%1: %2Past, Present and Future%1, Oxford.

%3Rescher,  Nicholas and Alasdair Urquhart (1971)%1: %2Temporal Logic%1,
Springer-Verlag, New York and Vienna.
.if false then begin
Notes

1979 March 30

What should be proved about airline program?

Another example where data structure is not specified?
Maybe topological sort?
(General example: do not treat an item that has been previously treated)

Can elephant idea be extended to interacting parallel programs?

1979 March 31

Suppose a function is computed by an elephant program.  How does one
define the function and prove its properties?  Example: append or reverse.

How is a program equivalent to one which is obtained from it by
introducing a new variable and computing it?  We need a concept of
equivalence of programs w/r set of variables.  

Parallel programs

	Consider the following Algolic program in which two processes
co-operate in finding the largest element of an array.

.begin nofill
%2 
∂9n := 1; b := 0;	∂(40)0
∂9qg l1,l2;∂(40)1
l1:∂9if n = N qthen qg done;∂(40)2
∂9b := max(b,a[n]);∂(40)3
∂9n := n + 1;∂(40)4
∂9qgl1;∂(40)5

l2:∂9if n = N qthen qg done;∂(40)2
∂9b := max(b,a[n]);∂(40)3
∂9n := n + 1;∂(40)4
∂9qgl2;∂(40)5

done:∂(40)6
.end

The intent is that the two programs share the variables ⊗b and ⊗n and
merge when they reach ⊗done.  It is also important that they not
interfere with each other.  We can describe this process using
the ideas of Elephant as follows:

It looks like the matching problem provides a conundrum for tense logic
and perhaps there should be a new tense giving the time that matches a
given time.

Inductive assertions

The partial correctness statement is

	%2∀t.(pc(t) = done ∧ ∀t'[0≤t'≤t ⊃ inprog pc(t')] ⊃ p(t) = m*n)%1

We prove by assuming %2pc(t) = done ∧ ∀t'[0≤t'≤t ⊃ inprog pc(t')]%1
and doing induction on

	%2qF(j) ≡ ∀t'[0 ≤ t - t' - 1 ≤ j ∧ pc(t') = start+2 ∧ p(t') = m*(n - i(t'))
⊃ p(t) = m*n]%1.

	qF(0) includes the condition ⊗t_-_t'_1_=_0, i.e. the program
must be just about to jump to ⊗done.  Therefore we must have ⊗i(t')_=_0 or
the program wouldn't jump, i.e. we wouldn't have ⊗pc(t)_=_pc(t'+1)_=_done.  From
this follows ⊗p(t')_=_m*n and consequently ⊗p(t)_=_m*n which was to
be proved.  If ⊗t'_=_t-1, the program, we can follow the program once
around the loop, see that the "invariant" is preserved and reduce the
problem to that for a smaller ⊗j.  Note that the induction is essentially
on time and we do not need to prove that ⊗i(t) decreases.
.end
.SKIP 1
This partial draft of ELEPHA[S80,JMC] compiled at {time} on {date}.